Termination Proof Script
Consider the TRS R consisting of the rewrite rule
1:
s1
(
s1
(
s0
(
s0
(x))))
→
s0
(
s0
(
s0
(
s1
(
s1
(
s1
(x))))))
There are 3 dependency pairs:
2:
S1
(
s1
(
s0
(
s0
(x))))
→
S1
(
s1
(
s1
(x)))
3:
S1
(
s1
(
s0
(
s0
(x))))
→
S1
(
s1
(x))
4:
S1
(
s1
(
s0
(
s0
(x))))
→
S1
(x)
Consider the SCC {2-4}.
The constraints could not be solved.
Tyrolean Termination Tool
(0.02 seconds) --- May 4, 2006